(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:
@(Cons(x, xs), ys) → Cons(x, @(xs, ys))
@(Nil, ys) → ys
binom(Cons(x, xs), Cons(x', xs')) → @(binom(xs, xs'), binom(xs, Cons(x', xs')))
binom(Cons(x, xs), Nil) → Cons(Nil, Nil)
binom(Nil, k) → Cons(Nil, Nil)
goal(x, y) → binom(x, y)
Rewrite Strategy: INNERMOST
(1) DecreasingLoopProof (EQUIVALENT transformation)
The following loop(s) give(s) rise to the lower bound Ω(2n):
The rewrite sequence
binom(Cons(x, xs), Cons(x', xs')) →+ @(binom(xs, xs'), binom(xs, Cons(x', xs')))
gives rise to a decreasing loop by considering the right hand sides subterm at position [0].
The pumping substitution is [xs / Cons(x, xs), xs' / Cons(x', xs')].
The result substitution is [ ].
The rewrite sequence
binom(Cons(x, xs), Cons(x', xs')) →+ @(binom(xs, xs'), binom(xs, Cons(x', xs')))
gives rise to a decreasing loop by considering the right hand sides subterm at position [1].
The pumping substitution is [xs / Cons(x, xs)].
The result substitution is [ ].
(2) BOUNDS(2^n, INF)
(3) RenamingProof (EQUIVALENT transformation)
Renamed function symbols to avoid clashes with predefined symbol.
(4) Obligation:
Runtime Complexity Relative TRS:
The TRS R consists of the following rules:
@(Cons(x, xs), ys) → Cons(x, @(xs, ys))
@(Nil, ys) → ys
binom(Cons(x, xs), Cons(x', xs')) → @(binom(xs, xs'), binom(xs, Cons(x', xs')))
binom(Cons(x, xs), Nil) → Cons(Nil, Nil)
binom(Nil, k) → Cons(Nil, Nil)
goal(x, y) → binom(x, y)
S is empty.
Rewrite Strategy: INNERMOST
(5) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)
Infered types.
(6) Obligation:
Innermost TRS:
Rules:
@(Cons(x, xs), ys) → Cons(x, @(xs, ys))
@(Nil, ys) → ys
binom(Cons(x, xs), Cons(x', xs')) → @(binom(xs, xs'), binom(xs, Cons(x', xs')))
binom(Cons(x, xs), Nil) → Cons(Nil, Nil)
binom(Nil, k) → Cons(Nil, Nil)
goal(x, y) → binom(x, y)
Types:
@ :: Cons:Nil → Cons:Nil → Cons:Nil
Cons :: Cons:Nil → Cons:Nil → Cons:Nil
Nil :: Cons:Nil
binom :: Cons:Nil → Cons:Nil → Cons:Nil
goal :: Cons:Nil → Cons:Nil → Cons:Nil
hole_Cons:Nil1_0 :: Cons:Nil
gen_Cons:Nil2_0 :: Nat → Cons:Nil
(7) OrderProof (LOWER BOUND(ID) transformation)
Heuristically decided to analyse the following defined symbols:
@,
binomThey will be analysed ascendingly in the following order:
@ < binom
(8) Obligation:
Innermost TRS:
Rules:
@(
Cons(
x,
xs),
ys) →
Cons(
x,
@(
xs,
ys))
@(
Nil,
ys) →
ysbinom(
Cons(
x,
xs),
Cons(
x',
xs')) →
@(
binom(
xs,
xs'),
binom(
xs,
Cons(
x',
xs')))
binom(
Cons(
x,
xs),
Nil) →
Cons(
Nil,
Nil)
binom(
Nil,
k) →
Cons(
Nil,
Nil)
goal(
x,
y) →
binom(
x,
y)
Types:
@ :: Cons:Nil → Cons:Nil → Cons:Nil
Cons :: Cons:Nil → Cons:Nil → Cons:Nil
Nil :: Cons:Nil
binom :: Cons:Nil → Cons:Nil → Cons:Nil
goal :: Cons:Nil → Cons:Nil → Cons:Nil
hole_Cons:Nil1_0 :: Cons:Nil
gen_Cons:Nil2_0 :: Nat → Cons:Nil
Generator Equations:
gen_Cons:Nil2_0(0) ⇔ Nil
gen_Cons:Nil2_0(+(x, 1)) ⇔ Cons(Nil, gen_Cons:Nil2_0(x))
The following defined symbols remain to be analysed:
@, binom
They will be analysed ascendingly in the following order:
@ < binom
(9) RewriteLemmaProof (LOWER BOUND(ID) transformation)
Proved the following rewrite lemma:
@(
gen_Cons:Nil2_0(
n4_0),
gen_Cons:Nil2_0(
b)) →
gen_Cons:Nil2_0(
+(
n4_0,
b)), rt ∈ Ω(1 + n4
0)
Induction Base:
@(gen_Cons:Nil2_0(0), gen_Cons:Nil2_0(b)) →RΩ(1)
gen_Cons:Nil2_0(b)
Induction Step:
@(gen_Cons:Nil2_0(+(n4_0, 1)), gen_Cons:Nil2_0(b)) →RΩ(1)
Cons(Nil, @(gen_Cons:Nil2_0(n4_0), gen_Cons:Nil2_0(b))) →IH
Cons(Nil, gen_Cons:Nil2_0(+(b, c5_0)))
We have rt ∈ Ω(n1) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
(10) Complex Obligation (BEST)
(11) Obligation:
Innermost TRS:
Rules:
@(
Cons(
x,
xs),
ys) →
Cons(
x,
@(
xs,
ys))
@(
Nil,
ys) →
ysbinom(
Cons(
x,
xs),
Cons(
x',
xs')) →
@(
binom(
xs,
xs'),
binom(
xs,
Cons(
x',
xs')))
binom(
Cons(
x,
xs),
Nil) →
Cons(
Nil,
Nil)
binom(
Nil,
k) →
Cons(
Nil,
Nil)
goal(
x,
y) →
binom(
x,
y)
Types:
@ :: Cons:Nil → Cons:Nil → Cons:Nil
Cons :: Cons:Nil → Cons:Nil → Cons:Nil
Nil :: Cons:Nil
binom :: Cons:Nil → Cons:Nil → Cons:Nil
goal :: Cons:Nil → Cons:Nil → Cons:Nil
hole_Cons:Nil1_0 :: Cons:Nil
gen_Cons:Nil2_0 :: Nat → Cons:Nil
Lemmas:
@(gen_Cons:Nil2_0(n4_0), gen_Cons:Nil2_0(b)) → gen_Cons:Nil2_0(+(n4_0, b)), rt ∈ Ω(1 + n40)
Generator Equations:
gen_Cons:Nil2_0(0) ⇔ Nil
gen_Cons:Nil2_0(+(x, 1)) ⇔ Cons(Nil, gen_Cons:Nil2_0(x))
The following defined symbols remain to be analysed:
binom
(12) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)
Could not prove a rewrite lemma for the defined symbol binom.
(13) Obligation:
Innermost TRS:
Rules:
@(
Cons(
x,
xs),
ys) →
Cons(
x,
@(
xs,
ys))
@(
Nil,
ys) →
ysbinom(
Cons(
x,
xs),
Cons(
x',
xs')) →
@(
binom(
xs,
xs'),
binom(
xs,
Cons(
x',
xs')))
binom(
Cons(
x,
xs),
Nil) →
Cons(
Nil,
Nil)
binom(
Nil,
k) →
Cons(
Nil,
Nil)
goal(
x,
y) →
binom(
x,
y)
Types:
@ :: Cons:Nil → Cons:Nil → Cons:Nil
Cons :: Cons:Nil → Cons:Nil → Cons:Nil
Nil :: Cons:Nil
binom :: Cons:Nil → Cons:Nil → Cons:Nil
goal :: Cons:Nil → Cons:Nil → Cons:Nil
hole_Cons:Nil1_0 :: Cons:Nil
gen_Cons:Nil2_0 :: Nat → Cons:Nil
Lemmas:
@(gen_Cons:Nil2_0(n4_0), gen_Cons:Nil2_0(b)) → gen_Cons:Nil2_0(+(n4_0, b)), rt ∈ Ω(1 + n40)
Generator Equations:
gen_Cons:Nil2_0(0) ⇔ Nil
gen_Cons:Nil2_0(+(x, 1)) ⇔ Cons(Nil, gen_Cons:Nil2_0(x))
No more defined symbols left to analyse.
(14) LowerBoundsProof (EQUIVALENT transformation)
The lowerbound Ω(n1) was proven with the following lemma:
@(gen_Cons:Nil2_0(n4_0), gen_Cons:Nil2_0(b)) → gen_Cons:Nil2_0(+(n4_0, b)), rt ∈ Ω(1 + n40)
(15) BOUNDS(n^1, INF)
(16) Obligation:
Innermost TRS:
Rules:
@(
Cons(
x,
xs),
ys) →
Cons(
x,
@(
xs,
ys))
@(
Nil,
ys) →
ysbinom(
Cons(
x,
xs),
Cons(
x',
xs')) →
@(
binom(
xs,
xs'),
binom(
xs,
Cons(
x',
xs')))
binom(
Cons(
x,
xs),
Nil) →
Cons(
Nil,
Nil)
binom(
Nil,
k) →
Cons(
Nil,
Nil)
goal(
x,
y) →
binom(
x,
y)
Types:
@ :: Cons:Nil → Cons:Nil → Cons:Nil
Cons :: Cons:Nil → Cons:Nil → Cons:Nil
Nil :: Cons:Nil
binom :: Cons:Nil → Cons:Nil → Cons:Nil
goal :: Cons:Nil → Cons:Nil → Cons:Nil
hole_Cons:Nil1_0 :: Cons:Nil
gen_Cons:Nil2_0 :: Nat → Cons:Nil
Lemmas:
@(gen_Cons:Nil2_0(n4_0), gen_Cons:Nil2_0(b)) → gen_Cons:Nil2_0(+(n4_0, b)), rt ∈ Ω(1 + n40)
Generator Equations:
gen_Cons:Nil2_0(0) ⇔ Nil
gen_Cons:Nil2_0(+(x, 1)) ⇔ Cons(Nil, gen_Cons:Nil2_0(x))
No more defined symbols left to analyse.
(17) LowerBoundsProof (EQUIVALENT transformation)
The lowerbound Ω(n1) was proven with the following lemma:
@(gen_Cons:Nil2_0(n4_0), gen_Cons:Nil2_0(b)) → gen_Cons:Nil2_0(+(n4_0, b)), rt ∈ Ω(1 + n40)
(18) BOUNDS(n^1, INF)